Nuprl Lemma : eq_knd_self 0,22
k:Knd. k = k ~ true 
latex

Definitionsb, t  T, x:A. B(x), a = b, P  Q, P  Q, P & Q, P  Q, Knd, , {T}, SQType(T), KindDeq
Lemmasdeq property, Kind-deq wf, bool sq, Knd wf, eqtt to assert, eq knd wf

origin